%Two facts about multibib:
%1) if you use \citeFoo{myref}, and the bib entry for myref contains
%\cite{my_second_ref}, then the \cite{my_second_ref} will be interpreted
%like a \citeFoo{my_second_ref}, i.e., it will cause an entry for my_second_ref
%to occur in the Foo-bibliography
%2) if you use \citeFoo{myref}, and the bib entry for myref contains
%\citeBar{my_second_ref}, then the \citeBar{my_second_ref} will create a reference
%to my_second_ref, and will  will cause an entry for my_second_ref
%to occur in the Bar-bibliography provided there is a
%\bibliographyBar command somewhere. If there is no \bibliographyBar anywhere, but
%there is a \citeBanana{my_second_ref} and \bibliographyBanana elsewhere, then
%\citeBar{my_second_ref} will create a reference to my_second_ref as it occurs in the
%Banana-bibligraphy.
%
%What does this mean for Gesamtpublikationsverzeichnis.tex:
%- To prevent 1) I should use \citeother, not \cite, in own_publications.bib
% Otherwise all conference papers cited in the entries for the TRs
% will be repeated in the Berichte bibliography.
%- There is no \bibliographyother command. Thus it is important that
%for any citeother commands within own_publications.bib, there is a
%\citeBar or \nociteBar somewhere

@mastersthesis{Sma96-masters,
  author = 	 {Jan-Georg Smaus},
  key =          {Abc},
  type =         {Diplomarbeit},
  title = 	 {Resolution {K}-Transformations},
  school = 	 {Universit{\"a}t des Saarlandes (Max-Planck-Institut f{\"u}r
   Informatik)},
  year = 	 1996
}

@techreport{SHK97-tr,
     author = {Jan-Georg Smaus and Patricia M. Hill and Andy King},
     title = {Domain Construction for Mode Analysis of Typed Logic Programs},
     institution = {Computing Laboratory, University of Kent at Canterbury, United Kingdom},
     year = 1997,
     number = {8-97},
     note = {Early version of~\cite{SHK00-lopstr}}   
}

@InProceedings{SHK97-poster,
  author = 	 {Jan-Georg Smaus and Patricia M. Hill and Andy King},
  title = 	 {Domain Construction for Mode Analysis of Typed Logic Programs},
  booktitle = 	 {Proceedings of the 14th Joint International Conference
                  and Symposium on Logic Programming},
  pages =	 418,
  year =	 1997,
  editor =	 {Lee Naish},
  publisher =	 {MIT Press},
  note =	 {Abstract of Poster Presentation}
}

@TechReport{Sma98-tr,
  author = 	 {Jan-Georg Smaus},
  title = 	 {Well-Terminating, Input-Driven Logic Programs},
  institution =  {University of Kent at Canterbury},
  year = 	 1998,
  number =	 {16-98},
  note = {Early version of~\cite{Sma99-iclp}}
}

@TechReport{SHK98-tr,
  author = 	 {Jan-Georg Smaus and Patricia M. Hill and Andy King},
  title = 	 {Verification of Logic Programs with {\tt block} Declarations
Running in Several Modes},
  institution =  {University of Kent at Canterbury},
  number = {7-98},
  year = 	 1998,
  address =	 {Canterbury, CT2~7NF, United Kingdom},
  month =	 {July},
  note =         {Contains proofs for~\cite{SHK98-plilp,SHK99-lopstr}; see also~\cite{SHK01}}
}

@InProceedings{SHK98-prelopstr,
  author = 	 {Jan-Georg Smaus and Patricia M. Hill and Andy King},
  title = 	 {Preventing Instantiation Errors and Loops
for Logic Programs with Several Modes Using {\tt block} Declarations},
  booktitle = 	 {Pre-Proceedings of the 8th International Workshop on Logic-based Program Synthesis and Transformation},
  year =	 1998,
  editor =	 {Pierre Flener},
  number =       {UMCS-98-6-1},
  publisher =	 {University of Manchester},
  pages =        {72--29},
  note =	 {Extended abstract}
}

@InProceedings{SHK98-plilp,
  author = 	 {Jan-Georg Smaus and Patricia M. Hill and Andy King},
  title = 	 {Termination of Logic Programs with {\tt block} Declarations
Running in Several Modes},
  booktitle = 	 {Proceedings of the 10th Symposium on Programming Language Implementations and Logic Programming},
  year =	 1998,
  editor =	 {Catuscia Palamidessi},
  series =	 {LNCS},
  pages =        {73--88},
  volume =       1490, 
  publisher =	 {Springer-Verlag}
}

@TechReport{KSH98-tr,
  author = 	 {Andy King and Jan-Georg Smaus and Patricia M. Hill},
  title = 	 {Practical
  Dependency Analysis through a ${S}hare$ Quotient},
  institution =  {Computing Laboratory, University of Kent},
  year = 	 1998,
  number =	 {11-98},
  note   =       {Early version of~\cite{KSH99}}
}

@PhdThesis{Sma99-phd,
  author = 	 {Jan-Georg Smaus},
  title = 	 {Modes and Types in Logic Programming},
  school = 	 {University of Kent at Canterbury},
  year = 	 1999
}

@PhdThesis{Sma99-phd-for-Uppsala,
  author = 	 {Jan-Georg Smaus},
  title = 	 {Modes and Types in Logic Programming},
  school = 	 {University of Kent at Canterbury},
  year = 	 1999,
  note =         {Based on \cite{SHK98-plilp,SHK99-lopstr,Sma99-iclp,SHK00-lopstr}}
}


@InProceedings{Sma99-iclp,
  author = 	 {Jan-Georg Smaus},
  title = 	 {Proving Termination of Input-Consuming Logic Programs},
  booktitle = 	 {Proceedings of the 16th International Conference
                  on Logic Programming},
  year =	 1999,
  editor =	 {Danny {De Schreye}},
  pages =        {335--349},
  publisher =	 {MIT Press}
}

@Proceedings{ES99,
  title = 	 {Proceedings of the Workshop on Verification of Logic
                  Programs held at ICLP'99},
  year = 	 1999,
  editor =	 {Sandro Etalle and Jan-Georg Smaus},
  volume =	 "30(1)",
  series =	 {Electronic Notes in Theoretical Computer Science},
  publisher =	 {Elsevier}
}

@InProceedings{SHK99-prelopstr,
  author = 	 {Jan-Georg Smaus and Patricia M. Hill and Andy King},
  title = 	 {Mode Analysis Domains for Typed Logic Programs},
  booktitle = 	 {Pre-Proceedings of the 9th International Workshop on 
                  Logic-based Program Synthesis and Transformation},
  year =	 1999,
  editor =	 {Annalisa Bossi},
  publisher =	 {Universit{\`a} C{\`a} Foscari di Venezia},
  note =	 {Extended abstract},
  pages =        {163--170}
}

@TechReport{Sma99-tr,
  author = 	 {Jan-Georg Smaus},
  title = 	 {Proving Termination of Input-Consuming Logic Programs},
  institution =  {Computing Laboratory, University of Kent at Canterbury, United Kingdom},
  year = 	 1999,
  number =	 {10-99},
  note =         {Long version of~\cite{Sma99-iclp}}
}

@InProceedings{KSH99,
  author = 	 {Andy King and Jan-Georg Smaus and Patricia M. Hill},
  title = 	 {Quotienting $\mathit{Share}$ for Dependency Analysis},
  booktitle = 	 {Proceedings of the 8th European Symposium on Programming},
  year =	 1999,
  volume =       1576,
  pages =        {59--73},
  editor =	 {Doaitse Swierstra},
  publisher =	 {Springer-Verlag},
  series =       {LNCS}
}

@InProceedings{SHK99-lopstr,
  author = 	 {Jan-Georg Smaus and Patricia M. Hill and Andy King},
  title = 	 {Preventing Instantiation Errors and Loops
for Logic Programs with Multiple Modes Using {\tt block} Declarations},
  booktitle = 	 {Proceedings of the 8th International Workshop on Logic-based Program Synthesis and Transformation},
  year =	 1999,
  pages =        {289--307},
  editor =	 {Pierre Flener},
  publisher =	 {Springer-Verlag},
  volume =       {1559},
  series =       {LNCS}
}

@InProceedings{DS00-jfplc,
  author = 	 {Jan-Georg Smaus and Pierre Deransart},
  title = 	 {Les programmes bien typ{\'e}s ont tout bon},
  booktitle = 	 {Proceedings of Journ{\'e}es Francophones de 
                  Programmation en Logique avec Contraintes},
  pages =	 {49--65},
  year =	 2000,
  editor =	 {Toura{\"\i}vane},
  publisher =	 {Hermes Science Publications}
}

@InProceedings{DS00-vcl,
  author = 	 {Jan-Georg Smaus and Pierre Deransart},
  title = 	 {Well-typed Programs Are not Wrong},
  booktitle = 	 {Verification and Computational Logic Workshop},
  year =	 2000,
  editor =	 {Michael Leuschel et al.},
  publisher =	 {Technical report DSEE-TR-2000-6 of the University of Southampton},
  note =	 {Held within CL'2000}
}

@TechReport{SHK00-tr,
  author = 	 {Jan-Georg Smaus and Patricia M. Hill and Andy King},
  title = 	 {Mode Analysis Domains for Typed Logic Programs},
  institution =  {University of Leeds},
  year = 	 2000,
  number =	 {2000.06},
  note =	 {Long version of~\cite{SHK00-lopstr}}
}

@InProceedings{SHK00-lopstr,
  author = 	 {Jan-Georg Smaus and Patricia M. Hill and Andy King},
  title = 	 {Mode Analysis Domains for Typed Logic Programs},
  booktitle = 	 {Proceedings of the 9th International Workshop on Logic-based Program Synthesis and Transformation},
  year =	 2000,
  editor =	 {Annalisa Bossi},
  series =	 {LNCS},
  pages =        {83--102},
  volume =       1817,
  publish =	 {Springer-Verlag}
}


@InProceedings{SFD00,
  author = 	 {Jan-Georg Smaus and Fran{\c c}ois Fages and Pierre Deransart},
  title = 	 {Using Modes to Ensure Subject Reduction for Typed Logic Programs with Subtyping},
  booktitle = 	 {Proceedings of the 20th Conference on the 
                  Foundations of Software Technology 
                  and Theoretical Computer Science},
  year =	 2000,
  publisher =      {Springer-Verlag},
  series =       {LNCS},
  volume =       {1974},
  pages =        {214--226},
  editor =       {Sanjiv Kapoor and Sanjiva Prasad},
}

@TechReport{SFD00-tr,
  author = 	 {Jan-Georg Smaus and Fran{\c c}ois Fages and Pierre Deransart},
  title = 	 {Using Modes to Ensure Subject Reduction for Typed Logic Programs with Subtyping},
  institution =  {INRIA},
  number =       {RR-4020},
  year = 	 2000,
  note =         {Long version of \cite{SFD00}, available via CoRR: {\tt http://arXiv.org/archive/cs/intro.html}}
}

@TechReport{BERS00,
  author = 	 {Annalisa Bossi and Sandro Etalle and Sabina Rossi and Jan-Georg Smaus},
  title = 	 {On the Semantics and Termination of Logic Programs with Dynamic Scheduling},
  institution =  {Universit{\`a} Ca' Foscari di Venezia},
  year = 	 2000,
  note =         {Early version of \cite{BERS01}},
  number =	 {CS2000-11}
}

@TechReport{DS00,
  author = 	 {Pierre Deransart and Jan-Georg Smaus},
  title = 	 {Well-Typed Logic Programs Are not Wrong},
  institution =  {INRIA},
  number =       {RR-4082},
  year = 	 2000,
  note =         {Long version of \cite{DS01}, available via CoRR: {\tt http://arXiv.org/archive/cs/intro.html}}
}

@InProceedings{DS01,
  author = 	 {Pierre Deransart and Jan-Georg Smaus},
  title = 	 {Well-Typed Logic Programs Are not Wrong},
  booktitle = 	 {Proceedings of the 5th International 
                  Symposium on Functional and Logic Programming},
  year =	 2001,
  editor =	 {Herbert Kuchen and Kazunori Ueda},
  series =	 {LNCS},
  publisher =	 {Springer-Verlag},
  pages =        {280--295},
  volume =       {2024}
}

@Article{SHK01,
  author = 	 {Jan-Georg Smaus and Patricia M. Hill and Andy King},
  title = 	 {Verifying
  Termination and Error-freedom of Logic Programs with {\tt block} Declarations},
  journal = 	 {Theory and Practice of Logic Programming},
  year = 	 2001,
  volume =       1,
  number =       4, 
  pages =        {447--486}
}


@InProceedings{BERS01,
  author = 	 {Annalisa Bossi and Sandro Etalle and Sabina Rossi and Jan-Georg Smaus},
  title = 	 {Semantics and Termination of Simply-Moded Logic Programs with Dynamic
  Scheduling},
  booktitle = 	 {Proceedings of the European Symposium on Programming},
  year =	 2001,
  editor =	 {David Sands},
  series =	 {LNCS},
  publisher =	 {Springer-Verlag},
  volume = 2028,
  pages = {402--416}  
}

@Unpublished{BERS01-tr,
  author = 	 {Annalisa Bossi and Sandro Etalle and Sabina Rossi and Jan-Georg Smaus},
  title = 	 {Semantics and Termination of Simply-Moded Logic Programs with Dynamic
  Scheduling},
  note = 	 {Long version of \cite{BERS01}, available via CoRR: 
                  {\tt http://arXiv.org/archive/cs/intro.html}},
  year =	 2001
}

@Article{AS01,
  author = 	 {Krzysztof R. Apt and Jan-Georg Smaus},
  title = 	 {Rule-based versus Procedure-based View of Logic Programming},
  journal = 	 {Joint Bulletin of the Novosibirsk Computing Center and Institute of
Informatics Systems; Series: Computer Science},
  year = 	 2001,
  volume =	 16,
  pages =        {75--97},
}

@Unpublished{Sma01-aci-corr,
  author = 	 {Jan-Georg Smaus},
  title = 	 {Analysis of Polymorphically Typed Logic Programs
                  Using {ACI}-Unification},
  note = 	 {Long version of \cite{Sma01-aci-lpar}, 
                  available via CoRR: {\tt http://arXiv.org/archive/cs/intro.html}},
  year =	 2001
}

@InProceedings{Sma01-aci-lpar,
  author = 	 {Jan-Georg Smaus},
  title = 	 {Analysis of Polymorphically Typed Logic Programs
                  Using {ACI}-Unification},
  booktitle = 	 {Proceedings of the 8th International Conference on
                  Logic for Programming, Artificial Intelligence and Reasoning},
  pages =	 {280--295},
  year =	 2001,
  editor =	 {Robert Nieuwenhuis and Andrei Voronkov},
  volume =	 2250,
  series =	 {LNAI},
  publisher =	 {Springer-Verlag}
}

@Article{PRS01,
  author = 	 {Dino Pedreschi and Salvatore Ruggieri and Jan-Georg Smaus},
  title = 	 {Classes of Terminating Logic Programs},
  journal = 	 {Theory and Practice of Logic Programming},
  year =         2001, 
  note =         {submitted}
}

@Article{PRS02,
  author = 	 {Dino Pedreschi and Salvatore Ruggieri and Jan-Georg Smaus},
  title = 	 {Classes of Terminating Logic Programs},
  journal = 	 {Theory and Practice of Logic Programming},
  year = 	 2002,
  volume =       {2},
  number =       {3},
  pages =        {369--418}
}

@Article{DS02,
  author = 	 {Pierre Deransart and Jan-Georg Smaus},
  title = 	 {Subject Reduction of Logic Programs as Proof-Theoretic Property},
  journal = 	 {Journal of Functional and Logic Programming 
                  (electronic journal)},
  publisher =    {EAPLS},  
  year =         {2002},
  volume=        {2002},
  number=        {2}
}

@Unpublished{BERS02,
  author = 	 {Annalisa Bossi and Sandro Etalle and Sabina Rossi and Jan-Georg Smaus},
  title = 	 {Semantics and Termination of Simply Moded Logic Programs with Dynamic  
  Scheduling},
  note = 	 {Submitted to TOCL}
}

@InProceedings{Sma02-flops,
  author = 	 {Jan-Georg Smaus},
  title = 	 {The Head Condition and Polymorphic Recursion},
  booktitle = 	 {Proceedings of the 6th International 
                  Symposium on Functional and Logic Programming},
  pages =	 {259--274},
  year =	 2002,
  editor =	 {Zhenjiang Hu and Mario Rodr{\'\i}guez-Artalejo},
  volume =	 2441,
  series =	 {LNCS},
  publisher =	 {Springer-Verlag}
}

@Unpublished{Sma02-tplp,
  author = 	 {Jan-Georg Smaus},
  title = 	 {The Optimality of {A}pt's Generic Semantics for First-Order Equations},
  note = 	 {Submitted to TPLP as Technical Note}
}

@Article{BERS03,
  author = 	 {Annalisa Bossi and Sandro Etalle and Sabina Rossi and Jan-Georg Smaus},
  title = 	 {Semantics and Termination of Simply Moded Logic Programs with Dynamic  
  Scheduling},
  journal = 	 {Transactions on Computational Logic},
  year = 	 2003,
  note =	 {Accepted}
}

@InProceedings{BKBetal03,
  author = 	 {Bernd Krieg-Br{\"u}ckner and Dieter Hutter and Arne Lindow and
                  Christoph L{\"u}th and Achim Mahnke and Erica Melis and Philipp Meier and
                  Arnd Poetzsch-Heffter and Markus Roggenbach and George Russell
                  and Jan-Georg Smaus and Martin Wirsing},
  title = 	 {MultiMedia Instruction in Safe and Secure Systems},
  booktitle = 	 {Recent Trends in Algebraic Development Techniques,
16th International Workshop, WADT 2002},
  pages =	 {82--117},
  year =	 2003,
  editor =	 {Martin Wirsing and Dirk Pattinson and Rolf Henecker},
  volume =	 {2755},
  series =	 {LNCS},
  publisher =	 {Springer-Verlag}
}

@InProceedings{Sma03-iclp,
  author = 	 {Jan-Georg Smaus},
  title = 	 {Is there an Optimal Generic Semantics for
                  First-Order Equations?},
  booktitle = 	 {Proceedings of the 19th International Conference on
                  Logic Programming},
  pages =	 {438--450},
  year =	 2003,
  editor =	 {Catuscia Palamidessi},
  series =	 {LNCS},
  volume =       {2916},
  publisher =	 {Springer-Verlag}
}

@InProceedings{Sma03-iclp-poster,
  author = 	 {Jan-Georg Smaus},
  title = 	 {Termination of Logic Programs for Various Dynamic
                  Selection Rules},
  booktitle = 	 {Proceedings of the 19th International Conference on
                  Logic Programming},
  pages =	 {511--512},
  year =	 2003,
  editor =	 {Catuscia Palamidessi},
  series =	 {LNCS},
  publisher =	 {Springer-Verlag},
  volume =       {2916},
  note =	 {Abstract of Poster Presentation}
}

@TechReport{SmaTR191-03,
  author = 	 {Jan-Georg Smaus},
  title = 	 {Termination of Logic Programs for Various Dynamic Selection Rules},
  institution =  {Institut f{\"u}r Informatik, Universit{\"a}t Freiburg},
  year = 	 2003,
  number =	 191
}

@TechReport{SmaTR203-04,
  author = 	 {Jan-Georg Smaus},
  title = 	 {Termination of Logic Programs Using Various Dynamic Selection Rules},
  institution =  {Institut f{\"u}r Informatik, Universit{\"a}t Freiburg},
  year = 	 2004,
  note =         {Long version of \cite{Sma04-iclp}},
  number =	 {203}
}

@Article{BERS04,
  author = 	 {Annalisa Bossi and Sandro Etalle and Sabina Rossi and Jan-Georg Smaus},
  title = 	 {Termination of Simply Moded Logic Programs with Dynamic  
  Scheduling},
  journal = 	 {Transactions on Computational Logic},
  year = 	 2004,
  volume =       5,
  number =       3,
  pages =        {470-507}
}

@InCollection{PRS04,
  author = 	 {Dino Pedreschi and Salvatore Ruggieri and Jan-Georg Smaus},
  title = 	 {Characterisations of Termination in Logic Programming},
  booktitle = 	 {Program Development in Computational Logic},
  publisher =	 {Springer-Verlag},
  year =	 2004,
  volume =       3049,
  editor =	 {Maurice Bruynooghe and Kung-Kiu Lau},
  series =	 {LNCS},
  pages =        {376--431}
}

@InProceedings{Sma04-iclp,
  author = 	 {Jan-Georg Smaus},
  title = 	 {Termination of Logic Programs Using Various Dynamic
                  Selection Rules},
  booktitle = 	 {Proceedings of the 20th International Conference on
                  Logic Programming},
  year =	 2004,
  editor =	 {Bart Demoen and Vladimir Lifschitz},
  series =	 {LNCS},
  volume =       {3132},
  publisher =	 {Springer-Verlag},
  pages =        {43-57}
}

@InProceedings{HofSmaRybKupPod06,
  author = 	 {J{\"o}rg Hoffmann and Jan-Georg Smaus and
                  Andrey Rybalchenko and Sebastian Kupferschmid and
                  Andreas Podelski},
  editor =       {Stefan Edelkamp and Alessio R. Lomuscio},   
  title = 	 {Using Predicate Abstraction to Generate Heuristic
                  Functions in {UPPAAL}},
  booktitle = 	 {Proceedings of the 4th Workshop on Model Checking
                  and Artificial Intelligence ({MoChArt} 2006)},
  year =	 2006
}

@InProceedings{RatSma06-preprints,
  author = 	 {Stefan Ratschan and Jan-Georg Smaus},
  editor =       {Christos G. Cassandras and Alessandro Giua and Carla
                  Seatzu and Janan Zaytoon},
  title = 	 {Verification-Integrated Falsification of Non-deterministic
Hybrid Systems},
  pages =        {371-376},
  booktitle = 	 {Preprints of the IFAC Conference on Analysis and
                  Design of Hybrid Systems},
  year = 2006,
  note = {Available via \url{http://www.diee.unica.it/~adhs06/CD/PAPERS/FB1.2.pdf}}
}

@InProceedings{RatSma06,
  author = 	 {Stefan Ratschan and Jan-Georg Smaus},
  editor =       {Christos G. Cassandras and Alessandro Giua and Carla
                  Seatzu and Janan Zaytoon},
  title = 	 {Verification-Integrated Falsification of Non-deterministic
Hybrid Systems},
  booktitle = 	 {Proceedings of the 2nd (2006) IFAC Conference on Analysis and
                  Design of Hybrid Systems},
  year = 2007,
  pages =        {371-376},
  publisher = {Elsevier Science Inc.},
}

@InProceedings{Sma-SAT+CP06,
  author = 	 {Jan-Georg Smaus},
  title = 	 {Representing {B}oolean Functions as Linear Pseudo-{B}oolean
  Constraints},
  booktitle = 	 {Proceedings of the {CP} 2006 Workshop on the
Integration of {SAT} and {CP} techniques},
  year =	 2006,
  pages =        {49-63},
  editor =	 {Youssef Hamadi}
}

@TechReport{SmaTR227-06,
  author = 	 {Jan-Georg Smaus},
  title = 	 {Representing {B}oolean Functions as Linear Pseudo-{B}oolean
                  Constraints},
  institution =  {Institut f{\"u}r Informatik, Universit{\"a}t Freiburg},
  year = 	 2006,
  number =	 227,
  note =         {Long version of \cite{Sma-SAT+CP06}}
}

@InProceedings{HofSmaRybKupPod07,
  author = 	 {J{\"o}rg Hoffmann and Jan-Georg Smaus and
                  Andrey Rybalchenko and Sebastian Kupferschmid and
                  Andreas Podelski},
  editor =       {Stefan Edelkamp and Alessio Lomuscio},   
  title = 	 {Using Predicate Abstraction to Generate Heuristic
                  Functions in {UPPAAL}},
  booktitle = 	 {Post-Proceedings of the 4th (2006) Workshop on Model Checking
                  and Artificial Intelligence},
  year =	 2007,
  series =	 {LNCS},
  pages     =    {51-66},
  volume    =    {4428},
  publisher =	 {Springer-Verlag}
}

@InProceedings{Sma-CPAIOR07,
  author = 	 {Jan-Georg Smaus},
  title = 	 {On {B}oolean Functions Encodable as a Single Linear Pseudo-{B}oolean
  Constraint},
  booktitle = 	 {Proceedings of the 4th International Conference on
        Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems},
  year =	 2007,
  editor =	 {Pascal Van Hentenryck and Laurence Wolsey},
  series =	 {LNCS},
  volume =       {4510},
  pages =        {288-302},
  publisher =	 {Springer-Verlag}
}

@TechReport{SmaTR230-07,
  author = 	 {Jan-Georg Smaus},
  title = 	 {On {B}oolean Functions Encodable as a Single Linear Pseudo-{B}oolean
  Constraint},
  institution =  {Institut f{\"u}r Informatik, Universit{\"a}t Freiburg},
  year = 	 2007,
  number =	 230,
  note = {Long version of \cite{Sma-CPAIOR07}. Also available as TR No.~13 on \url{http://www.avacs.org/}}
}

@TechReport{SmaTR230-07nocite,
  author = 	 {Jan-Georg Smaus},
  title = 	 {On {B}oolean Functions Encodable as a Single Linear Pseudo-{B}oolean
  Constraint},
  institution =  {Institut f{\"u}r Informatik, Universit{\"a}t Freiburg},
  year = 	 2007,
  number =	 230,
  note = {Long version of \cite{Sma-CPAIOR07}. Also available as TR No.~13 on http://www.avacs.org/}
}

@InProceedings{SmaHof07-withdrawn,
  author = 	 {Jan-Georg Smaus and J{\"o}rg Hoffmann},
  title = 	 {Relaxation Refinement: A New Method to Generate
                  Heuristic Functions},
  booktitle = 	 {Proceedings of the 14th International Workshop on
Model Checking Software (SPIN)},
  year =	 2007,
  editor =	 {Dragan Bosnacki and Stefan Edelkamp},
  publisher =	 {Springer-Verlag},
  note =	 {To appear}
}

@InProceedings{SmaHof09,
  author = 	 {Jan-Georg Smaus and J{\"o}rg Hoffmann},
  editor =	 {Doron Peled and Michael Wooldridge},
  title = 	 {Relaxation Refinement: A New Method to Generate
                  Heuristic Functions},
  booktitle = 	 {Post-Proceedings of the 5th (2008) Workshop on Model Checking
                  and Artificial Intelligence},
  year =	 2009,
  series =	 {LNCS},
  volume =       {5348},
  pages =        {147-165},
  publisher =	 {Springer-Verlag}
}

@InProceedings{RatSma08,
  author = 	 {Stefan Ratschan and Jan-Georg Smaus},
  title = 	 {Finding Errors of Hybrid Systems by Optimising 
 an Abstraction-Based Quality Estimate},
  editor =       {Tarmo Uustalu and J{\"u}ri Vain},
  booktitle = 	 {Proceedings of the 20th Nordic Workshop on Programming Theory},
  pages =        {72-74},
  year =	 2008
}

@InProceedings{BadLeuSma09,
  author = 	 {Bahareh Badban and Stefan Leue and Jan-Georg Smaus},
  title = 	 {Automated Invariant Generation for the Verification
                  of Real-Time Systems},
  booktitle = 	 {Proceedings of the 2nd International Workshop on
                  Invariant Generation},
  year =	 2009,
  proceedings =  {3-15},
  editor =	 {Andrew Ireland and Laura Kov{\'a}cs}
}


@PhdThesis{Sma09-habil,
  author = 	 {Jan-Georg Smaus},
  title = 	 {Logic and Abstraction, Verification and Falsification},
  school = 	 {Albert-Ludwigs-Universit{\"a}t Freiburg},
  year = 	 2009,
  type =	 {Habilitationsschrift},
  note =	 {Consists of a 51-page Summary and the articles 
                  \cite{PRS02,DS02,BERS04,SFD00,BERS01,
Sma01-aci-lpar,Sma02-flops,Sma03-iclp,Sma04-iclp,
                          RatSma06,HofSmaRybKupPod07,
                          Sma-CPAIOR07,SmaHof09,PRS04,Sma-SAT+CP06}}
}

@InProceedings{RatSma09,
  author = 	 {Stefan Ratschan and Jan-Georg Smaus},
  editor =	 {Catherine Dubois},
  title = 	 {Finding Errors of Hybrid Systems by Optimising 
 an Abstraction-Based Quality Estimate},
  booktitle = 	 {Proceedings of the 3rd International Conference on Tests and Proofs},
  year =	 2009,
  pages =        {153-168},
  series =	 {LNCS},
  volume =       {5668},
  publisher =	 {Springer-Verlag}
}

@techreport{RatSma09-tr51,
    author      =   {Stefan Ratschan and Jan-Georg Smaus},
    title       =   {Finding Errors of Hybrid Systems by Optimising
                     an Abstraction-Based Quality Estimate},
    editor      =   {Bernd Becker and Werner Damm and Martin Fr{\"a}nzle and
                     Ernst-R{\"u}diger Olderog and Andreas Podelski and Reinhard
                     Wilhelm},
    institution =   {SFB/TR 14 AVACS},
    subproject  =   {H1/2},
    year        =   {2009},
    type        =   {Reports of SFB/TR 14 AVACS},
    series      =   {ATR},
    number      =   51,
    note        =   {ISSN: 1860-9821, http://www.avacs.org. Long
                  version of \cite{RatSma09}},
    access      =   {open},
    abstract    = {We present an algorithm for falsifying safety
                   properties of hybrid systems, i.e., for finding a
                   trajectory to an unsafe state.  The approach is to
                   approximate how close a point is to being an
                   initial point of an error trajectory using a
                   real-valued quality function, and then to use
                   numerical optimisation to search for an optimum of
                   this function. The function is computed by running
                   simulations, where information coming from
                   abstractions computed by a verification algorithm
                   is exploited to determine whether a simulation
                   looks promising and should be continued or
                   cancelled. This information becomes more reliable
                   as the abstraction becomes more refined. We thus
                   interleave falsification and verification
                   attempts. In contrast to related work, we
                   consider hybrid systems with completely
                   deterministic evolution.}
}

@InProceedings{SchMerSma09,
  author = 	 {Alexander Schimpf and Stephan Merz and Jan-Georg Smaus},
  editor =       {Stefan Berghofer and Tobias Nipkow and Christian
                  Urban and Makarius Wenzel},
  title = 	 {Construction of {B}{\"u}chi Automata for {LTL} Model Checking Verified in {I}sabelle/{HOL}},
  booktitle = 	 {Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics},
  year =	 2009,
  pages =        {424-439},
  series =	 {LNCS},
  volume =       {5674},
  publisher =	 {Springer-Verlag}
}

@ARTICLE{BadLeuSma09-infinity,
  author = {Bahareh Badban and Stefan Leue and Jan-Georg Smaus},
  title = {Automated Predicate Abstraction for Real-Time Models},
  journal = {EPTCS},
  volume = {10},
  pages = {36-43},
  url = {doi:10.4204/EPTCS.10.3},
  year = {2009},
  editor =	 { Axel Legay and Azadeh Farzan},
  note = {Presented at INFINITY 2009, 11th International Workshop on Verification of Infinite-State Systems}
}

@Proceedings{MeySma11,
  title = 	 {Proceedings of the 6th Workshop on Model Checking
                  and Artificial Intelligence ({MoChArt} 2010)},
  year = 	 2011,
  editor =	 {Ron van der Meyden and Jan-Georg Smaus},
  volume =	 6572,
  series =	 {LNCS/LNAI},
  publisher =	 {Springer-Verlag}
}

%All up to here are considered in CV

@inproceedings{SmaSchWen12,
  author    = {Jan-Georg Smaus and
               Christian Schilling and
               Fabian Wenzelmann},
  title     = {Implementations of two algorithms for the threshold synthesis
               problem},
  booktitle = {International Symposium on Artificial Intelligence and Mathematics
               (ISAIM 2012), Fort Lauderdale, Florida, USA, January 9-11,
               2012},
  year      = {2012}
}

@InProceedings{SchSmaWen13,
  author = 	 {Christian Schilling and
                  Jan-Georg Smaus and
                  Fabian Wenzelmann},
  title = 	 {A Pretty Complete Combinatorial Algorithm for the
Threshold Synthesis Problem},
  booktitle = 	 {International Workshop on Combinatorial Algorithms},
  year =	 2013,
  editor =	 {T. Lecroq and L. Mouchard},
  series =	 {LNCS},
  publisher =	 {Springer-Verlag},
  note =	 {To appear}
}

@inproceedings{EspLamNeuNipSchSma13,
  author    = {Javier Esparza and
               Peter Lammich and
               Ren{\'e} Neumann and
               Tobias Nipkow and
               Alexander Schimpf and
               Jan-Georg Smaus},
  editor    = {Natasha Sharygina and
               Helmut Veith},
  booktitle     = {Computer Aided Verification - 25th International Conference,
               CAV 2013, Saint Petersburg, Russia, July 13-19,
                  2013. Proceedings},
  title     = {A Fully Verified Executable LTL Model Checker},
  year      = {2013},
  pages     = {463-478},
  publisher = {Springer-Verlag},
  series    = {LNCS},
  volume    = {8044}
}

@Unpublished{FraHerSma05,
  author = 	 {Martin Fr{\"a}nzle and Christian Herde and Jan-Georg Smaus},
  title = 	 {``{I}gnoring Delete Lists'' in Bounded Model Checking},
  note = 	 {Draft},
  year =	 2005
}

@Unpublished{KupSma05,
  author = 	 {Sebastian Kupferschmid and Jan-Georg Smaus},
  title = 	 {Pattern Database Heuristics for Reachability Analysis in Timed
  Automata},
  note = 	 {Discussion basis},
  year =	 {2005?}
}


@InProceedings{SmaHof08,
  author = 	 {Jan-Georg Smaus and J{\"o}rg Hoffmann},
  editor =	 {Doron Peled and Michael Wooldridge},
  title = 	 {Relaxation Refinement: A New Method to Generate
                  Heuristic Functions},
  booktitle = 	 {Submitted to MoChArt},
  year = {2008}
}

